PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 14:29:42 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 mapk_cascade.prism mapk_cascade.props --property reactions -const 'N=4,T=30'
Parsing model file "mapk_cascade.prism"...
Type: CTMC
Modules: E1 E2 KPTASE KKPTASE MAPK MAPKK MAPKKK
Variables: e1 e2 kptase kkptase k k_kkpp kp kp_kkpp kp_ptase kpp kpp_ptase kk kk_kkkp kkp kkp_kkkp kkp_ptase kkpp kkpp_ptase kkk kkk_e1 kkkp kkkp_e2
Parsing properties file "mapk_cascade.props"...
3 properties:
(1) "activated_T": R{"activated"}=? [ I=T ]
(2) "activated_time": R{"time"}=? [ F kpp=N ]
(3) "reactions": R{"reactions"}=? [ C<=T ]
---------------------------------------------------------------------
Model checking: "reactions": R{"reactions"}=? [ C<=T ]
Model constants: N=4
Property constants: T=30
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Model constants: N=4
Computing reachable states...
Reachability (BFS): 44 iterations in 3.44 seconds (average 0.078273, setup 0.00)
Time for model construction: 3.691 seconds.
Type: CTMC
States: 99535 (1 initial)
Transitions: 910872
Rate matrix: 111563 nodes (14 terminal), 910872 minterms, vars: 58r/58c
Computing rewards...
Engine: Sparse
Building sparse matrix... [n=99535, nnz=910872, compact] [3.6 MB]
Creating vector for diagonals... [dist=127, compact] [195.4 KB]
Allocating iteration vectors... [3 x 777.6 KB]
TOTAL: [6.0 MB]
Uniformisation: q.t = 2142.000000 x 30.000000 = 64260.000000
Fox-Glynn: left = 62483, right = 66413
Starting iterations...
Iteration 1323 (of 66413): max relative diff=0.003025, 5.00 sec so far
Iteration 2645 (of 66413): max relative diff=0.001452, 10.01 sec so far
Iteration 3952 (of 66413): max relative diff=0.000928, 15.01 sec so far
Iteration 5274 (of 66413): max relative diff=0.000659, 20.01 sec so far
Iteration 6597 (of 66413): max relative diff=0.000496, 25.01 sec so far
Iteration 7896 (of 66413): max relative diff=0.000389, 30.02 sec so far
Iteration 9220 (of 66413): max relative diff=0.000311, 35.02 sec so far
Iteration 10543 (of 66413): max relative diff=0.000253, 40.02 sec so far
Iteration 11865 (of 66413): max relative diff=0.000208, 45.02 sec so far
Iteration 13189 (of 66413): max relative diff=0.000173, 50.02 sec so far
Iteration 14493 (of 66413): max relative diff=0.000145, 55.02 sec so far
Iteration 15815 (of 66413): max relative diff=0.000122, 60.03 sec so far
Iteration 17140 (of 66413): max relative diff=0.000103, 65.03 sec so far
Iteration 18465 (of 66413): max relative diff=0.000087, 70.03 sec so far
Iteration 19788 (of 66413): max relative diff=0.000074, 75.04 sec so far
Iteration 21112 (of 66413): max relative diff=0.000063, 80.04 sec so far
Iteration 22435 (of 66413): max relative diff=0.000053, 85.04 sec so far
Iteration 23758 (of 66413): max relative diff=0.000045, 90.04 sec so far
Iteration 25084 (of 66413): max relative diff=0.000038, 95.05 sec so far
Iteration 26401 (of 66413): max relative diff=0.000032, 100.05 sec so far
Iteration 27727 (of 66413): max relative diff=0.000027, 105.05 sec so far
Iteration 29052 (of 66413): max relative diff=0.000023, 110.05 sec so far
Iteration 30370 (of 66413): max relative diff=0.000019, 115.05 sec so far
Iteration 31695 (of 66413): max relative diff=0.000016, 120.06 sec so far
Iteration 33014 (of 66413): max relative diff=0.000014, 125.06 sec so far
Iteration 34338 (of 66413): max relative diff=0.000013, 130.06 sec so far
Iteration 35656 (of 66413): max relative diff=0.000012, 135.06 sec so far
Iteration 36979 (of 66413): max relative diff=0.000011, 140.07 sec so far
Iteration 38300 (of 66413): max relative diff=0.000010, 145.07 sec so far
Iteration 39622 (of 66413): max relative diff=0.000010, 150.07 sec so far
Iteration 40941 (of 66413): max relative diff=0.000009, 155.07 sec so far
Iteration 42266 (of 66413): max relative diff=0.000009, 160.08 sec so far
Iteration 43591 (of 66413): max relative diff=0.000009, 165.08 sec so far
Iteration 44915 (of 66413): max relative diff=0.000008, 170.08 sec so far
Iteration 46236 (of 66413): max relative diff=0.000008, 175.08 sec so far
Iteration 47556 (of 66413): max relative diff=0.000008, 180.09 sec so far
Iteration 48877 (of 66413): max relative diff=0.000008, 185.09 sec so far
Iteration 50201 (of 66413): max relative diff=0.000008, 190.09 sec so far
Iteration 51526 (of 66413): max relative diff=0.000007, 195.09 sec so far
Iteration 52845 (of 66413): max relative diff=0.000007, 200.09 sec so far
Iteration 54167 (of 66413): max relative diff=0.000007, 205.09 sec so far
Iteration 55490 (of 66413): max relative diff=0.000006, 210.09 sec so far
Iteration 56810 (of 66413): max relative diff=0.000006, 215.10 sec so far
Iteration 58134 (of 66413): max relative diff=0.000006, 220.10 sec so far
Iteration 59456 (of 66413): max relative diff=0.000005, 225.10 sec so far
Iteration 60780 (of 66413): max relative diff=0.000005, 230.10 sec so far
Iteration 62102 (of 66413): max relative diff=0.000005, 235.11 sec so far
Iteration 63502 (of 66413): max relative diff=0.000004, 240.11 sec so far
Iteration 64932 (of 66413): max relative diff=0.000004, 245.11 sec so far
Iteration 66361 (of 66413): max relative diff=0.000004, 250.12 sec so far
Iterative method: 66413 iterations in 251.95 seconds (average 0.003769, setup 1.65)
Value in the initial state: 48.49102760677303
Time for model checking: 251.937 seconds.
Result: 48.49102760677303 (value in the initial state)
Overall running time: 256.222 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.